es-independent(es; i; k; x)
== s1,s2:es_state(es; i).
== es-x-equiv(es; i; x; s1; s2)
==  ((v:es-kindtype(es; i; k). 
==  es-x-equiv(es; i; x; (es-trans(es; i)(k,v,s1)); (es-trans(es; i)(k,v,s2)))
==   (es-send(es; i)(k,v,es-read-state(s1)) = es-send(es; i)(k,v,es-read-state(s2))))
==   ((islocal(k))
==    (n:. 
==    es-choose(es; i)(act(k),n,es-read-state(s1))
==    =
==    es-choose(es; i)(act(k),n,es-read-state(s2))))) 

latex

---

clarification:

es-independent(es; i; k; x)
== s1:es_state(es; i), s2:es_state(es; i).
== es-x-equiv(es; i; x; s1; s2)
==  ((v:es-kindtype(es; i; k). 
==  es-x-equiv(es; i; x; (es-trans(es; i)(k,v,s1)); (es-trans(es; i)(k,v,s2)))
==   (es-send(es; i)(k,v,es-read-state(s1))
==   (=
==   (es-send(es; i)(k,v,es-read-state(s2))
==   ( (es-Msg(es) List)))
==   ((islocal(k))
==    (n:. 
==    es-choose(es; i)(act(k),n,es-read-state(s1))
==    =
==    es-choose(es; i)(act(k),n,es-read-state(s2))
==     (es-kindtype(es; i; k) + Unit)))) 

latex

Definitions	es_state(es; i), P  Q, es-x-equiv(es; i; x; s1; s2), es-trans(es; i), type List, es-Msg(es), es-send(es; i), P  Q, b, islocal(k), x:A. B(x), , s = t, left + right, es-kindtype(es; i; k), Unit, f(a), es-choose(es; i), act(k), es-read-state(s)
FDL editor aliases	es-independent